Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(nil,y)  → y
2:    app(add(n,x),y)  → add(n,app(x,y))
3:    reverse(nil)  → nil
4:    reverse(add(n,x))  → app(reverse(x),add(n,nil))
5:    shuffle(nil)  → nil
6:    shuffle(add(n,x))  → add(n,shuffle(reverse(x)))
There are 5 dependency pairs:
7:    APP(add(n,x),y)  → APP(x,y)
8:    REVERSE(add(n,x))  → APP(reverse(x),add(n,nil))
9:    REVERSE(add(n,x))  → REVERSE(x)
10:    SHUFFLE(add(n,x))  → SHUFFLE(reverse(x))
11:    SHUFFLE(add(n,x))  → REVERSE(x)
The approximated dependency graph contains 3 SCCs: {7}, {9} and {10}.
Tyrolean Termination Tool  (0.02 seconds)   ---  May 4, 2006